FDL - Step of Proof: rfunction_void

Step of Proof: rfunction_void_wf

12,41

Inference at *
Iof proof for Lemma rfunction void wf:

{f | x:Void

Void}

Type

by ((With

i,j. True MemCD)

CollapseTHEN (Try (((Auto_aux (first_nat 1:n) ((first_nat 1:n

C),(first_nat 3:n)) (first_tok :t) inil_term))

CollapseTHEN (Fail))

))

C1: .....eq aux..... NILNIL

C1:

WellFnd{1}(Void;u,v.(

i,j. True)(u,v))

Definitions t T